sublist(T; L1; L2)
== f:int_seg(0; ||L1||)int_seg(0; ||L2||)
== (increasing(f; ||L1||)  (j:int_seg(0; ||L1||). L1[j] = L2[(f(j))])) 

latex

---

clarification:

sublist(T; L1; L2)
== f:int_seg(0; ||L1||)int_seg(0; ||L2||)
== (increasing(f; ||L1||)  (j:int_seg(0; ||L1||). L1[j] = L2[(f(j))]  T)) 

latex

Definitions	x:A. B(x), x:AB(x), P  Q, increasing(f; k), x:A. B(x), int_seg(i; j), #$n, ||as||, s = t, l[i], f(a)
FDL editor aliases	sublist